home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / p6b.clin2 < prev    next >
Text File  |  1992-04-03  |  1KB  |  52 lines
  1. % In a ring, if x*x*x=x for all x in the ring, then xy=yx for all x and y in
  2. % the ring.
  3.  
  4. assign(clause_splitting,3).
  5. assign(restricted_equality_transform,0).
  6. assign(support_list,[f]).
  7. assign(time_limit,20000).
  8.  
  9. set(auto_orient).
  10. set(constrained_rewriting).
  11. set(delete_all_instances).
  12. set(early_tautology_test).
  13. set(early_unit_subsumption).
  14. set(equality_transform).
  15. set(equational_rewrite).
  16. set(group_detection).
  17. set(include_original_clause).
  18. clear(precompute_constraints).
  19. set(replacement).
  20. clear(safe_early_priority_test).
  21. %clear(save_rewrite_rules).
  22. clear(save_unrestricted_normal_form).
  23. set(size_by_clause).
  24. set(slidepriority).
  25.  
  26. set(outrwr).
  27. set(outcsplit).
  28. set(outtreq).
  29. %set(outrwt).
  30. %set(outCacg).
  31.  
  32. user_rewrite.
  33.   g(1) > f(2).
  34.   f(2) > j(2).
  35. end.
  36.  
  37. axiom_list(sprfn).
  38.   j(0,X)=X.                      % 0 is a left identity for sum
  39.   j(X,0)=X.                      % 0 is a right identity for sum
  40.   j(g(X),X)=0.                   % there exists a left inverse for sum
  41.   j(X,g(X))=0.                   % there exists a right inverse for sum
  42.   j(j(X,Y),Z)=j(X,j(Y,Z)).       % associativity of addition
  43.   j(X,Y)=j(Y,X).                 % commutatvity of addition
  44.   f(f(X,Y),Z)=f(X,f(Y,Z)).       % associativity of multiplication
  45.   f(X,j(Y,Z))=j(f(X,Y),f(X,Z)).  % distributivity axiom
  46.   f(j(Y,Z),X)=j(f(Y,X),f(Z,X)).  % distribitivity axiom
  47.   f(X,f(X,X))=X.                 % special hypothesis
  48.   false :- f(a,b)=f(b,a).        % denial of the theorem
  49. end.
  50.  
  51. end_of_input.
  52.